% ----- load protocol files ---------------------------------------------------

loadfiles :-
  forall(load(X),
   (string_to_atom(S1,X),
    string_concat('protocols/',S1,S2),
    string_concat(S2,'.pro',S3),
    [S3])).


% ----- instantiation of items ------------------------------------------------

di(X,Y) :- role(_,init,LST), member(X:Y,LST), Y\=di.

institem(DOM,cm(DI,[PR],dot),X,ctxm(DOM,PR,DI,X,Y)) :- di(X,Y), !. % data item (contents given)
institem(DOM,cm(DI,[PR],dot),X,ctxm(DOM,PR,DI,X,c:X)) :- !.      % data item (default contents)
institem(DOM,cm(ID,[PR],_),X,ctxm(DOM,PR,ID,X,X)).              % identifier

institem(DOM,cm(NO,dot,bot),ctxm(DOM,dot,NO,i:DOM:NO,c:DOM:NO)). % nonce


instmsg(_,_,[],[]).
instmsg(P,I,[X|LST],[XR|LSTR]) :- instmsg(P,I,X,XR), instmsg(P,I,LST,LSTR).
instmsg(P,I,pri(T,LST),pri(T,LSTR)) :- instmsg(P,I,LST,LSTR).
instmsg(PR,INST,cmr(V,P1,P2),RET) :- member(V=Y,INST), !, institem(PR,cmr(V,P1,P2),Y,RET).
instmsg(PR,_,cmr(V,P1,P2),RET) :- institem(PR,cmr(V,P1,P2),RET).
instmsg(PR,INST,cm(V,P1,P2),RET) :- member(V=Y,INST), !, institem(PR,cm(V,P1,P2),Y,RET).
instmsg(PR,_,cm(V,P1,P2),RET) :- institem(PR,cm(V,P1,P2),RET).

instinit(U,IX,X:di,ctxm((dot,U),IX,X,X,c:X)) :- !.
instinit(U,IX,X:Y, ctxm((dot,U),IX,X,X,Y)) :- !.
instinit(U,IX,X,   ctxm((dot,U),IX,X,X,X)) :- !.




% ----- print initial knowledge -----------------------------------------------

printpr(U,PROF,IX) :-
  forall(member(X,PROF),
    (print('knows('),print(U),print(','),
     instinit(U,IX,X,OUT),print(OUT),print(').\n'))).

printprs(_,[],_).
printprs(U,[X|LST],IX) :-
  printpr(U,X,IX),
  IXP1 is IX+1,
  printprs(U,LST,IXP1).

printinit(U) :-
  findall(PR,role(U,init,PR),ALLPR),
  printprs(U,ALLPR,1).


% ----- print protocol knowledge ----------------------------------------------

printknows(_,init,_) :- !.

printknows(U,PR,R) :-
  proto(PR,TYPE,INST),
  forall(protoknow(TYPE,R,M),
    (print('knows('),print(U),print(','),
     instmsg(PR,INST,M,MP),print(MP),
     print(').\n'))).
%  print(U),print(PR),print(R),print('\n').


printknows(U) :-
  printinit(U),
  forall(role(U,PR,R),printknows(U,PR,R)).

printknows :-
  findall(U,role(U,_,_),LSTU), list_to_set(LSTU,SETU),
  forall(member(U,SETU), printknows(U)).
